{-# LANGUAGE GADTs #-}

module Vector where

import Representation



data Vector a n where
  VNil :: Vector a Z
  VCons :: a -> Vector a n -> Vector a (S n)

vHead :: Vector a (S n) -> a
vHead (VCons a _) = a

vTail :: Vector a (S n) -> Vector a n
vTail (VCons _ as) = as

vAppend :: Vector a n -> Vector a m -> Vector a (Add n m)
vAppend VNil = id
vAppend (VCons a as) = VCons a . vAppend as

vToList :: Vector a n -> [a]
vToList VNil = []
vToList (VCons a as) = a : vToList as
